Nuprl Lemma : q-rel-lub_wf
11,40
postcript
pdf
r1
,
r2
:
. q-rel-lub(
r1
;
r2
)
latex
Definitions
q-rel-lub(
r1
;
r2
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
band
wf
,
eq
int
wf
,
ifthenelse
wf
origin
r1, r2:
. q-rel-lub(r1;r2) 
r1, r2:. q-rel-lub(r1;r2) Tx:A. B(x)